p:FinProbSpace, A:(p-open(p)), s:(Outcome).
(i:. s  A(i))  s  countable-p-union(i.A(i)) 

latex

Definitions

s  C, x:A  B(x), x:A. B(x), FinProbSpace, t  T, x:A. B(x), p-open(p), , Type, x:AB(x), Outcome, f(a), x(s), , P  Q, {x:A| B(x)} , True, b, b, A  B, i z j, , s = t, T, P  Q, P  Q, Unit, left + right, <a, b>, False, A, , Void, #$n, n+m, i <z j, if b then t else f fi , a < b, P & Q, {i..j}, S  T, i  j < k, suptype(S; T), x. t(x), countable-p-union(i.A(i)), A c B, imax-list(L), (i = j), upto(n), x.A(x), map(f;as), (xL.P(x)), ||as||, x:A.B(x), Top, (x  l), xL. P(x), {T}, i  j

Lemmas

imax-list wf, all functionality wrt iff, implies functionality wrt iff, imax-list-lb, member upto2, member map, l member wf, imax-list-ub, map wf, length-map, upto wf, length upto, assert of bnot, not functionality wrt iff, assert of eq int, eq int wf, not wf, countable-p-union wf, int seg wf, ifthenelse wf, eqtt to assert, assert of lt int, iff transitivity, eqff to assert, squash wf, true wf, bnot of lt int, assert of le int, lt int wf, bool wf, le int wf, le wf, assert wf, bnot wf, p-open-member wf, p-outcome wf, nat wf, p-open wf, finite-prob-space wf